/*
 * $Id: ProtocolListener.java 2233 2007-04-18 14:49:48Z kofron $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Pavel Parizek <parizek@nenya.ms.mff.cuni.cz>
 * 
 */
package org.objectweb.fractal.bpc.jpf;

import java.util.List;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.Map;
import java.util.HashMap;
import java.util.Stack;
import java.util.Set;
import java.util.HashSet;
import java.util.Iterator;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.GenericProperty;
import gov.nasa.jpf.PropertyListenerAdapter;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.search.SearchListener;

import gov.nasa.jpf.jvm.Transition;
import gov.nasa.jpf.jvm.Step;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.StackFrame;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
import gov.nasa.jpf.jvm.bytecode.ReturnInstruction;
import gov.nasa.jpf.jvm.bytecode.ATHROW;


import org.objectweb.fractal.bpc.checker.DFSR.JPFTraverser;


public class ProtocolListener extends PropertyListenerAdapter
{
    // stack of transitions is necessary for correct handling of backtracking
	private Stack transitions = null;
	
    // map of strings of the form '<className>.<methodName>' to names of events that occur in the protocol
	private Map methods2events = null;	
	
    // set of names of classes that implement server interfaces
    private Set serverClasses = null;
    
    private JPFTraverser traverser = null;
    
    private boolean checkFailed = false;
    private boolean endStateOccured = false;
    private boolean errorReported = false;
 
    // statistics
    private int uniqueStates = 0;
    private int visitedStates = 0;
    
    
    /**
     * @param itf2class map of names of interfaces to names of classes that implement them.
     * @param serverItfs list of names of fractal server interfaces.
     * @param events list of events that should be passed to the BP checker.
     */
	public ProtocolListener(JPFTraverser tr, Map itf2class, Set serverItfs, String[] events)
	{
		transitions = new Stack();
		
		methods2events = createMethods2Events(itf2class, events);
        
        serverClasses = createServerClasses(serverItfs, itf2class);
        
        this.traverser = tr;
	}
	
    public Set getMethodNames()
    {
        if (this.methods2events == null) return new HashSet();
        
        return this.methods2events.keySet();
    }
    
    
	public void stateAdvanced(Search search) 
	{
		//System.err.println("State advanced");
	
        if (search.isNewState()) uniqueStates++;
        visitedStates++;
        
		Transition tr = search.getTransition();
		List ptr = extractProtocolTransition(tr);
		
		transitions.push(ptr);

		moveForward(ptr);
        
        if (search.isEndState())
        {
            endStateOccured = true;
            
            if (!traverser.notifyEnd()) checkFailed = true;
        }
	}
	
	public void stateBacktracked(Search search) 
	{
		//System.err.println("State backtracked");

		List ptr = (List) transitions.pop();
	
		moveBackward(ptr);
	}

	public void stateProcessed(Search search) 
    {
        //System.err.println("State processed");
        
        if (search.isEndState())
        {
            endStateOccured = true;
            
            if (!traverser.notifyEnd()) checkFailed = true;
        }
    }
	
    public void searchFinished(Search search)
    {
        //System.err.println("Search finished");
        
        /*
        if (search.isEndState())
        {
            endStateOccured = true;
            
            if (!traverser.notifyEnd()) checkFailed = true;
        }
        */
        
        if ((!checkFailed) && (!endStateOccured))
        {
            System.err.println("Warning: no end state occured - there is probably an infinite loop or a deadlock in the code");
        }
        
        System.err.println("Unique states: " + uniqueStates);
        System.err.println("Visited states: " + visitedStates);
    }


	public void instructionExecuted(JVM vm)
	{
		Instruction instr = vm.getLastInstruction();
		ThreadInfo ti = vm.getLastThreadInfo(); 

		//System.err.println("instr: type = "+instr.getClass().getName()+", location = " + instr.getFileLocation());

		if (instr instanceof InvokeInstruction)
		{
			InvokeInstruction invokeInstr = (InvokeInstruction) instr;
			
			MethodInfo mi = invokeInstr.getInvokedMethod();

			String className = getClassName(mi);
			String methodName = getMethodName(mi);
                
			String fullMethodName = className + "." + methodName;

			//System.err.println("invoke: " + fullMethodName);
				
            String event = (String) methods2events.get(fullMethodName);
            if (event != null) 
			{
				// event != null -> protocol event occured -> break transition
				ti.breakTransition();
			}
		}
		else if (instr instanceof ReturnInstruction)
		{
			MethodInfo mi = instr.getMethodInfo();

			String className = getClassName(mi);
			String methodName = getMethodName(mi);
                
			String fullMethodName = className + "." + methodName;

			//System.err.println("return: " + fullMethodName);
				
            String event = (String) methods2events.get(fullMethodName);
            if (event != null) 
			{
				// event != null -> protocol event occured -> break transition
				ti.breakTransition();
			}
		}
	}
 
    public boolean check(Search search, JVM vm)
    {
        if (errorReported) return true;

        if (checkFailed) errorReported = true;
        
        return !checkFailed;
    }
    
    public String getErrorMessage()
    {
        return "Tested component is not compliant with the protocol";
    }

    
	/* utility methods */

	private void moveForward(List protoTrans)
	{
        // walk through all steps in this transition from the 'oldest' to the most 'recent one'
		for (int i = 0; i < protoTrans.size(); i++)
		{
			Object protoEvent = protoTrans.get(i);
		
			if (protoEvent instanceof ProtocolInvoke)
			{
				ProtocolInvoke protoInv = (ProtocolInvoke) protoEvent;
					
				//System.err.println("fw proto inv: " + protoInv.event);
                
				if (!checkFailed)
				{
					if (!traverser.notifyForwardInvoke(protoInv.thread, protoInv.isClientEvent, protoInv.event)) checkFailed = true;
				}
			}
			else if (protoEvent instanceof ProtocolReturn)
			{
				ProtocolReturn protoRet = (ProtocolReturn) protoEvent;
				
				//System.err.println("fw proto ret: " + protoRet.event);
                 
				if (!checkFailed)
				{
					if (!traverser.notifyForwardReturn(protoRet.thread, protoRet.isClientEvent, protoRet.event)) checkFailed = true;
				}
			}
		}
	}

	private void moveBackward(List protoTrans)
	{
		for (int i = protoTrans.size() - 1; i >= 0; i--)
		{
			Object protoEvent = protoTrans.get(i);
		
			if (protoEvent instanceof ProtocolInvoke)
			{
				ProtocolInvoke protoInv = (ProtocolInvoke) protoEvent;
					
				//System.err.println("bw proto inv: " + protoInv.event);
                
				if (!checkFailed)
				{
					if (!traverser.notifyBackwardInvoke(protoInv.thread, protoInv.isClientEvent, protoInv.event)) checkFailed = true;
				}
			}
			else if (protoEvent instanceof ProtocolReturn)
			{
				ProtocolReturn protoRet = (ProtocolReturn) protoEvent;
				
				//System.err.println("bw proto ret: " + protoRet.event);
                 
				if (!checkFailed)
				{
					if (!traverser.notifyBackwardReturn(protoRet.thread, protoRet.isClientEvent, protoRet.event)) checkFailed = true;
				}
			}
		}
	}

	private List extractProtocolTransition(Transition trans)
	{
		List protoTrans = new ArrayList();
		
        // walk through all steps in this transition from the 'oldest' to the most 'recent one'
		for (Iterator it = trans.iterator(); it.hasNext(); )
		{
			Step step = (Step) it.next();
		
			Instruction instr = step.getInstruction();

			if (instr instanceof InvokeInstruction)
			{
				InvokeInstruction invokeInstr = (InvokeInstruction) instr;
			
				MethodInfo mi = invokeInstr.getInvokedMethod();

				String className = getClassName(mi);
				String methodName = getMethodName(mi);
                
				String fullMethodName = className + "." + methodName;
				
                //System.err.println("inv: " + fullMethodName);

            	String event = (String) methods2events.get(fullMethodName);
               	if (event != null) 
				{
					// event != null -> we are interested in this event
					
					ProtocolInvoke protoInv = new ProtocolInvoke(trans.getThreadIndex(), !serverClasses.contains(className), event);
					
					protoTrans.add(protoInv);
				}
			}
			else if (instr instanceof ReturnInstruction)
			{
				MethodInfo mi = instr.getMethodInfo();

				String className = getClassName(mi);
				String methodName = getMethodName(mi);
                
				String fullMethodName = className + "." + methodName;
				
                //System.err.println("ret: " + fullMethodName);

                String event = (String) methods2events.get(fullMethodName);
                if (event != null) 
				{
					// event != null -> we are interested in this event
					
					ProtocolReturn protoRet = new ProtocolReturn(trans.getThreadIndex(), !serverClasses.contains(className), event);

					protoTrans.add(protoRet);
				}
			}
			else if (instr instanceof ATHROW)
			{
				// TODO
				
				// here we assume that there exist a next instruction (this should be always true as the ATHROW instruction is not scheduling relevant, etc)
			}
		}

		return protoTrans;
	}


	private String getClassName(MethodInfo mi)
	{
		if (mi == null) return "";
		if (mi.getClassInfo() == null) return "";

		return mi.getClassInfo().getName();
	}

	private String getMethodName(MethodInfo mi)
	{
		if (mi == null) return "";

		return mi.getName();
	}
    
    private Map createMethods2Events(Map itf2class, String[] events)
    {
        Map m2e = new HashMap();
     
        for (int i = 0; i < events.length; i++)
        {
            String event = events[i];
            
            String evItf = "";
            String evMethod = "";
            int k = event.indexOf('.');
            if (k != -1)
            {
                evItf = event.substring(0, k);
                evMethod = event.substring(k+1);
            }
            
            String evClass = (String) itf2class.get(evItf);
            
            if ((evClass != null) && (evMethod.length() > 0))
            {     
                m2e.put(evClass+"."+evMethod, event);
            }
        }
        
        return m2e;
    }
    
    private Set createServerClasses(Set serverItfs, Map itf2class)
    {
        Set sc = new HashSet();
        
        for (Iterator it = serverItfs.iterator(); it.hasNext(); )
        {
            String itf = (String) it.next();
            
            String cls = (String) itf2class.get(itf);
            if (cls != null) sc.add(cls);
        }
        
        return sc;
    }
    
	class ProtocolInvoke
	{
		protected int thread;
		protected boolean isClientEvent;
		protected String event;

		ProtocolInvoke(int thread, boolean isClientEvent, String event)
		{
			this.thread = thread;
			this.isClientEvent = isClientEvent;
			this.event = event;
		}

	}

	class ProtocolReturn
	{
		protected int thread;
		protected boolean isClientEvent;
		protected String event;

		ProtocolReturn(int thread, boolean isClientEvent, String event)
		{
			this.thread = thread;
			this.isClientEvent = isClientEvent;
			this.event = event;
		}

	}

}
